Inference at * 1 1 1 
Iof proof for Lemma p-fun-exp-add1-sq:



1. A : Type
2. f : A(A + Top)
3. x : A
4. isl(f(x))
  (f(x)) ~ (inl outl(f(x)) ) 

latex

 by (MoveToConcl (-1)) 
CollapseTHEN (((GenConclAtAddr [1;1;1]) 
CollapseTHENA (Auto)) 

CoCollapseTHEN ((D (-2)) 
CollapseTHEN ((Reduce 0) 
CollapseTHEN (Auto)))) 

latex

C.

Definitions

f(a), Top, s = t, x:A. B(x), x:AB(x), t  T, left + right, True, b, P  Q, False